M:MsgA. Feasible(M)  AtomFree(Type;M.state) 

latex

Definitions	x. t(x), t  T, State(ds), 1of(t), M.state, P  Q, x:A. B(x), x(s), Valtype(da;k), M.rframe(A.sends tfL of k on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), 2of(t), P & Q, Feasible(M), MsgA, Prop
Lemmas	msga wf, ma-feasible wf, fpf wf, top wf, id-deq wf, fpf-cap wf, Id wf, atom-free-fpf, atom-free-Id